
\existentialConstants {
  int c0, c1, c2, c3, c4, c5, c6, c7, c8, c9;
}

\problem {
  \exists int x3; \forall int x2; \exists int x1; \exists int x0; (
         5*x0 + 19*x1 + -15*x2 + -6*x3 + 6*c7 + 3*c5 + 9*c3 + -4*c2 + -36*c1 = 0
       & 38*x1 + -16*x2 + -9*x3 + 9*c7 + -4*c5 + 11*c3 + -8*c2 + -54*c1 = 0
       & 10*c5 + 9*c3 = 0
       & 37*x0 + 5*x2 + x3 + 9*c7 + -2*c3 + -3*c2 != 0
       & 9*x0 + 7*c8 + -17*c7 + -14*c5 + 9*c3 + 19*c2 != 0
       & 8*x0 + -6*x3 + 14*c5 + 15*c1 + -9 != 0
       & 7*x0 + 7*x3 + -3*c2 + 13*c1 != 0
       & 6*x0 + -14*x1 + 6*x2 + 11*x3 + 12*c8 + 32*c7 + -14*c2 + 19*c1 != 0
       & 16*x1 + -2*c8 + 17*c7 + 10*c5 + -23*c2 + 19*c1 != 0
       & 12*x3 + 20*c7 + 12*c3 + -1*c2 + 15 != 0
       & c3 != 0)
}